the_es:ES, j:E.
(isrcv(j))
 (snds(lnk(j), before(sender(j),index(j))) = []  ((Msg on lnk(j)) List))
 (msgs(lnk(j);before(j)) = []  (Msg List)) 

latex

Definitions

x:A. B(x), P  Q, t  T, , Top, S  T, A, P  Q, P & Q, x:A. B(x), {i..j}, i  j < k, A  B, False, {T}, (x  l), , A c B, T, True, (Msg on l), haslink(l;m), Dec(P), P  Q, P  Q, emsg(e), mlnk(m), msg(l;t;v), t.1, ||as||, Y

Lemmas

es-Msgl wf, es-lnk wf, es-snds-index wf, es-sender wf, es-index wf, int seg wf, length wf1, es-sends wf, assert wf, es-isrcv wf, es-E wf, event system wf, decidable assert, null wf3, es-msgs wf, top wf, assert of null, not functionality wrt iff, es-Msg wf, member exists, member-es-msgs, assert-es-haslnk, es-axioms, member-es-snds-index, le wf, select wf, int seg properties, es-locl wf, l member wf, haslink wf2, non neg length, squash wf, true wf, IdLnk wf, mlnk wf2